;;;; Created on 2012-11-21 20:20:07


(defun eval-truth-orig (&optional interpretation sentence)
  "Evaluate the truth of the sentence under an interpretation.
  The interpretation is a list of (proposition . truth-value) pairs,
  where a truth-value is t or nil, e.g., ((P . t) (Q . nil)).
  It is an error if there are any propositional symbols in the sentence
  that are not given a value in the interpretation."
  (write-line (format nil "interp: ~a" interpretation))
  (write-line (format nil "sent ~a" interpretation))
  (write-line (format nil "ops ~a" (op sentence)))
  (write-line (format nil "sublis: ~a" (sublis interpretation sentence)))
  
  ;(cond (interpretation (eval-truth (sublis interpretation sentence) nil))
  (cond (interpretation (eval-truth (sublis interpretation sentence) nil))
    
    ((eq sentence 'true) t)
    ((eq sentence 'false) nil)
    ((atom sentence) (error "No interpretation for ~A." sentence))
    ;(t (case (op sentence)
    (t (case (op sentence)
         (or  (some #'eval-truth (args sentence)))
         (and (every #'eval-truth (args sentence)))
         (not (not (eval-truth (arg1 sentence))))
         (IMPLIES  (or (eval-truth (arg2 sentence))
                       (not (eval-truth (arg1 sentence)))))
         (EQUIV (eq (eval-truth (arg1 sentence))
                    (eval-truth (arg2 sentence))))
         (otherwise (error "Unknown connective ~A in ~A"
                   (op sentence) sentence))))
    ))


(defun TruthValue (sentence &optional interpretation)
  "Evaluate the truth of the sentence under an interpretation.
  The interpretation is a list of (proposition . truth-value) pairs,
  where a truth-value is t or nil, e.g., ((P . t) (Q . nil)).
  It is an error if there are any propositional symbols in the sentence
  that are not given a value in the interpretation."
  (let ((truthval (sublis interpretation sentence)))
  (write-line (format nil "StartOf TruthValue" ))
  (write-line (format nil "interpre: ~a" interpretation))
  (write-line (format nil "sentence ~a" sentence))
  (write-line (format nil "ops ~a" (op sentence)))
  (write-line (format nil "intops ~a" (op interpretation)))
  ;(write-line (format nil "sublis: ~a" (sublis sentence interpretation )))
  (write-line (format nil "truthval: ~a" truthval))
  (write-line (format nil "============================"))
  (write-line (format nil "operand ~a" (op sentence)))
  (write-line (format nil "opercar ~a" (op (car sentence))))
  (write-line (format nil "============================"))
  (cond 
    (interpretation (TruthValue (sublis sentence interpretation) nil))
    ;((eq sentence 'true) t)
    ;((eq (op (car sentence)) t) t)
    ((eq (op sentence) t) t)
    ;((eq (op (car sentence)) 'true) t)
    
    ;((eq sentence 'false) nil)
    ((eq (op (car sentence)) nil) 
      ;(write-line (format nil "FALSE!"))
      nil)
    ((atom sentence) (error "No interpretation for ~A." sentence))
    (t 
      ;(case (op (car sentence))
      (case (op sentence)
        (or  (some #'TruthValue (args sentence)))
        (and 
          ;(write-line (format nil "AND!")) 
          (every #'TruthValue (args sentence))
          ;(every #'TruthValue (args truthval))
        )
        (NOT 
          (write-line (format nil "NOT! --~a" (arg1 sentence)))
          (not (TruthValue (arg1 sentence)))
        )
        (IMPLIES  (or (TruthValue (arg2 sentence))
          (not (TruthValue (arg1 sentence)))))
        (EQUIV (eq (TruthValue (arg1 sentence))
          (TruthValue (arg2 sentence))))
        (otherwise 
          (error "Unknown connective ~A in ~A" (op sentence) sentence)
          ;(write-line (format nil "ERROR!! Unknown connective ~A in ~A" (op sentence) sentence))
          nil
        )))
    )))



;original
(defun TruthValue (sentence &optional interpretation)
  "Evaluate the truth of the sentence under an interpretation.
  The interpretation is a list of (proposition . truth-value) pairs,
  where a truth-value is t or nil, e.g., ((P . t) (Q . nil)).
  It is an error if there are any propositional symbols in the sentence
  that are not given a value in the interpretation."
  ;(let ((truthval (sublis interpretation sentence))) 
;  (write-line (format nil "StartOf TruthValue" ))
;  (write-line (format nil "interpre: ~a" interpretation))
;  (write-line (format nil "sentence ~a" sentence))
;  (write-line (format nil "ops ~a" (op sentence)))
;  (write-line (format nil "intops ~a" (op interpretation)))
;  (write-line (format nil "sublis: ~a" (sublis sentence interpretation )))
;  (write-line (format nil "truthval: ~a" truthval))
;  (write-line (format nil "============================"))
;  (write-line (format nil "operand ~a" (op sentence)))
;  (write-line (format nil "opercar ~a" (op (car sentence))))
;  (write-line (format nil "============================"))
  (cond 
    (interpretation (TruthValue (sublis sentence interpretation) nil))
    ;((eq sentence 'true) t)
    ((eq (op (car sentence)) t) t)
    ;((eq (op (car sentence)) 'true) t)
    
    ;((eq sentence 'false) nil)
    ((eq (op (car sentence)) nil) 
       ;(write-line (format nil "FALSE!"))
       nil)
    ((atom sentence) (error "No interpretation for ~A." sentence))
    (t 
     
     (case (op (car sentence))
       (or  (some #'TruthValue (args sentence)))
       (and 
         ;(write-line (format nil "AND!")) 
         (every #'TruthValue (args sentence))
         ;(every #'TruthValue (args truthval))
       )
       (NOT 
;        (write-line (format nil "NOT! --~a" (arg1 sentence)))
        (not (TruthValue (arg1 sentence)))
       )
       (IMPLIES  (or (TruthValue (arg2 sentence))
         (not (TruthValue (arg1 sentence)))))
       (EQUIV (eq (TruthValue (arg1 sentence))
         (TruthValue (arg2 sentence))))
       (otherwise 
         (error "Unknown connective ~A in ~A" (op sentence) sentence)
         ;(write-line (format nil "ERROR!! Unknown connective ~A in ~A" (op sentence) sentence))
         nil
       )))
    ))





(defun is-alltermsp (x)
  (write-line  (format nil "list: ~a" (listp x)))
  (cond 
    ((listp x)
      (dolist (dox x)
      (write-line  (format nil "List!"))
      (print (get-length x))
      (cond
        ((eq (get-length x) 0)
         (print "len=0")
          nil)
        ((eq (get-length x) 1)
          (print "len=1")
          (if (termp (stringify (car x)))
              t
              nil))
        ((> (get-length x) 1)
          (print "len>1")
          (if (termp (stringify (car x)))
              (is-alltermsp (cdr x))
              nil))
))
   ((eq (listp x) nil)
     (print "notlist"))
  )))
  
  
  
(defun is-alltermsp (x)
  (write-line  (format nil "list: ~a" (listp x)))
  (cond 
    ((listp x)
      (dolist (dox x)
      (write-line  (format nil "List! ~a    Len:~a" dox (get-length dox)))
      (cond
        ((eq (get-length dox) 0)
         (write-line  (format nil "len=0 ~a" dox))
         (write-line  (format nil "return:~a"(termp (stringify dox))))
         (if (termp (stringify dox))
              t
              nil))
        ((eq (get-length dox) 1)
          (write-line  (format nil "len=1 ~a" dox))
          (if (termp (stringify (car dox)))
              t
              nil))
        ((> (get-length dox) 1)
          (write-line  (format nil "len>1 ~a" dox))
          (if (termp (stringify (car dox)))
              (is-alltermsp (cdr dox))
              nil))
)))
   ((eq (listp x) nil)
     (print "notlist"))
  ))
  
  
  
  (defun wfp-checkerFOL (wfp)
  "Checks to see if the argument is a correct well formed proposition."
  (write-line (format nil "----------------------------" ))
  (write-line  (format nil "sentence:~a" wfp))
  (if (atom wfp)  
    (write-line (format nil "Atom-wfp: ~a" wfp) (nil))           ; means its a proposition
    (case (car wfp)               ; else check whether its a particular type of wfp
      ;==========================================
      ((or and) ;conjunction/disjunction
        (write-line  (format nil "Or Condition:~a -- NIL" wfp))
        (wfp-FOL-listp (cdr wfp)))    ; check if each of its arguments is a wfp
      ;==========================================
      (not  ;;negated
        (if (= (length wfp) 2)           ;; make sure the length is correct and its argument is a wfp
            (write-line  (format nil "AND Condition:~a -- NIL" wfp))
            (wfp-checkerFOL (second wfp)))
          nil)
      ;==========================================
      ((IMPLIES) ; implications
        (write-line  (format nil "IMPLIES Condition:~a -- NIL" wfp))
        (if (= (length wfp) 3)     ; make sure the length is correct and the arguments are all wfps
           (wfp-FOL-listp (cdr wfp)))
         nil)
      ;==========================================
      ;((EQUIV iff) ; Equivalences
      (EQUIV  ; Equivalences
        (if (= (length wfp) 3)     ; make sure the length is correct and the arguments are all wfps
            (write-line  (format nil "EQUIV Condition:~a -- NIL" wfp))
            (wfp-FOL-listp (cdr wfp)))
          nil)
      ;==========================================
      ((ALL) ; implications
       (if (= (length wfp) 3)     ; make sure the length is correct and the arguments are all wfps
           (write-line  (format nil "ALL Condition:~a -- NIL" wfp))
           (wfp-FOL-listp (cdr wfp)))
         nil)
      ;==========================================
      ((EXISTS) ; implications
       (if (= (length wfp) 3)     ; make sure the length is correct and the arguments are all wfps
           (write-line  (format nil "EXISTS Condition:~a -- NIL" wfp))
           (wfp-FOL-listp (cdr wfp)))
         nil)
      ;==========================================
      (otherwise            ; its a proposition
        ;; But make sure that the first element of the proposition is an
        ;; atom.  We do not support lists as the predicate name
        (write-line (format nil "============================"))
        (write-line (format nil "Length: ~a" (length  wfp)))
        (write-line  (format nil "wfp:     ~a" wfp ))
;        (write-line  (format nil "listp ~a" (listp wfp)))
        (write-line  (format nil "op      : ~a" (op wfp)))
        (write-line  (format nil "car     : ~a  : ~a" (get-length (car wfp)) (car wfp) ))
        (write-line  (format nil "cdr     : ~a  : ~a" (get-length (cdr wfp)) (cdr wfp) ))
        (write-line  (format nil "arg1    : ~a  : ~a" (get-length (arg1 wfp)) (arg1 wfp) ))
        (write-line  (format nil "arg2    : ~a  : ~a" (get-length (arg2 wfp)) (arg2 wfp) ))
        (write-line  (format nil "len>1?  : ~a" (len>1? wfp) ))
        (write-line  (format nil "islen>1 : ~a" (> (length wfp) 1)))
        (write-line (format nil "============================"))
;        (cond
;           ((len>1? wfp)   ; Length of wfp is too Long
;            (write-line  (format nil "list: ~a" wfp))
;            (write-line  (format nil "cdr: ~a" (cdr wfp)))
;            (dolist (item wfp)
;              (term-type (stringify item))
;              (write-line  (format nil "item:~a" item))
;            )
;        )
;          )
        (cond
;          ((len>1? wfp)   ; Length of wfp is too Long
;            (write-line  (format nil "Too Long!-t:~a -- NIL" (car wfp)))
;            nil
;          )
          ;==========================================
          ((eq (predicatep (stringify (op wfp))) t)
          ;((eq (predicatep (stringify (arg1 wfp))) t)
            (write-line (format nil "____________________"))
            (write-line  (format nil "Predicate???: ~a   len: ~a" (op wfp) (get-length wfp)))
            (if (> (get-length wfp) 1)
              ;(wfp-FOL-listp (arg1 wfp))
              (wfp-checkerFOL (cdr wfp))
              t))
          ;==========================================
          ((eq (termp (stringify (arg1 wfp))) t)
            (write-line  (format nil "len wfp: ~a" (get-length wfp)))
            (write-line (format nil "____________________"))
            (write-line  (format nil "Term!: ~a" (arg1 wfp)))
            (if (= (length wfp) 1)
              t
              ;(wfp-FOL-listp (car wfp))
          ))
          ;==========================================
          ((eq (funcp (stringify (arg1 wfp))) t)
            (write-line (format nil "____________________"))
            (write-line  (format nil "Func! :~a" (arg1 wfp)))
            (if (> (get-length wfp) 1)
              (wfp-FOL-listp (cdr wfp))
              nil))
          ;==========================================
          
;          ((eq (listp wfp) nil) ; does not have paren's around pred
;            (write-line (format nil "not list!: ~a" (car wfp)))
;            nil
;          )
          ;==========================================
;          ((len>1? wfp)   ; Length of wfp is too Long
            ;(let ((retvar nil)))
;            (write-line  (format nil "list: ~a" wfp))
;            (write-line  (format nil "cdr: ~a" (cdr wfp)))
;           (write-line  (format nil "list-->predicate: ~a" (listp wfp)))
           ;eq (listp wfp) nil
           
;            (dolist (item wfp)
;              (term-type (stringify item))
;              (write-line  (format nil "item:~a" item))
;            )
;            (wfp-checkerFOL (cdr wfp))
;            t
;          )
          ;==========================================
          ((and (eq (atom (car wfp)) t) (eq (listp wfp) t) (eq (case? (stringify (car wfp))) t))
            t
          )
        )
))))





;=============================================================


(setf start-state
  '((side cat left)
    (side rat left)
    (side grain left)
    (side farmer left)
    (side boat left)
    (empty(boat))))

;Constants: 
;a - cat, 
;b - rat, 
;c - grain, 
;d - farmer, 
;e - boat, 
;S = side
;E = empty
;
()

(setf start-state
  '((S |a| |u|)
    (S |b| |u|)
    (S |c| |u|)
    (S |d| |u|)
    (S |e| |u|)
    (S (|e|))))


;Goal
(setf goal-state
  '((SIDE |cat| |right|)
    (side rat right)
    (side grain right)
    (side farmer right)
    (side boat right)
    (empty(boat))))

(setf operators
  '(
    ;ACTION
    ((moveboat X)   ; move boat to x side
    ;PRECOND
    ((side boat (NOT X)) (inboat farmer))
    ;ADD
    ((side boat X))
    ;DELETE
    ((side boat (NOT X))))
    
    ;ACTION
    ((unload X Y)           ; unload x item on y side
    ;PRECOND
    ((side boat Y) (inboat X) (not (empty boat)))
    ;ADD
    ((side X Y))
    ;DELETE
    ((inboat X)))

    ;ACTION
    ((load X Y)             ; unload x item from y side
    ;PRECOND
    ((side boat Y) (side X Y) (NOT (capacity boat)))
    ;ADD
    ((inboat X))
    ;DELETE
    ((side X Y)))
))
